% Topics in this section:
% 1. What's access control policies 2. Integrity of access control policies 3.
% APN model construction for implementing functionality and security 4.
% Transforming access control policies into model properties 5. Proof of
% properties insuring the coverage of system functionality and security

% !TEX root =  acl_resilience.tex

In this paper, we use OrBAC~\cite{citeulike:1362491, DBLP:conf/issre/TraonMB07,
DBLP:conf/policy/KalamBMBCSBDT03, DBLP:journals/entcs/CuppensCG07} to describe
access control policies, which guarantee the confidentiality and safety of
systems. An access control policy can be a permission or prohibition of an
access to a certain system resource in a specific context, e.g.
\emph{Permission(Student, Borrow, Book, WorkingDays)}.

A significant issue of access control policies is the \emph{integrity}. In
general, all accesses to system resources should be explicitly defined as
``allowed'' or ``blocked'', without any ambiguity. There are simple principles
to insure the integrity. Since system behaviors and resources - ``Borrow'' and
``Book'' respectively in the above example - are normally coupled deeply as a
system function, we may check the completeness of the accesses on these coupled
functions by enumerating variant accesses of different combinations of roles and
contexts, ``Student'' and ``WorkingDays'' respectively in the above example.
After we achieved the complete accesses sets of functions, we assert control
policy to each access by adding the proposition, either \emph{Permission} or
\emph{Prohibition}, and insure that permissions and prohibitions are disjoint.

Formally we have
\begin{align*}
PERM_f \cap PROH_f = \phi \\
|PERM_f| + |PROH_f| = |R \times C|
\end{align*}
where $PERM_f$/$PROH_f$ is the set of permissions/prohibitions on a specific
function \emph{f} respectively; \emph{R} is the set of roles and \emph{C} is the
set of contexts that applying to this function \emph{f}.

To model the kind of systems with access control policies by APN, we propose a
set of basic principles to organize the model construction, which may well
integrate the elements of access control policies with system functionality:
\begin{itemize}
  \item Model system activities into transitions. Be aware if one activity could
  lead the system to several states under different conditions, then build
  transitions for each of these conditions.
  \item Build places, with corresponding ADTs, to store instances (tokens)
  of roles, resources and contexts separately.
  \item Regarding the activities on which there are access control policies
  defined, the input places of the corresponding transitions should at least
  contain the ones which store the related users, resources and access
  conditions.
  \item If any transition of these secure activity fires, the output arc should
  generate a special token called ``log'' which records system access
  information.
  \item Supplement the model with other necessary transitions, places and etc,
  which are not security-related, to implement full functionality of the system.
\end{itemize}

In the above principles, a log is an instance of an access control policy in the
runtime, which records the concrete data of the elements of the system access.
Afterwards we can verify the model by checking that every marking in the state
space whether violates any access control policy. In particular, we are
interested in checking either of the following:
\begin{enumerate}
  \item for all recorded accesses to a certain activity, at least one of the activity's permissions is met;
  \item for all recorded accesses to a certain activity, none of the prohibitions for that activity is met.
\end{enumerate}

If the integrity of the access control policy is insured, it's sufficient to
verify either point above for the system safety, which insures each access is
authorized.
In the following context, we continue our reasoning by relying solely on
permission verification, the point 1 above. Formally, for a given activity
\emph{act}, we define the terms of temporal logic as:
\begin{align*}
\bold{AG}(\forall t \in act\_log : Perm_{1}^{act} (t) \vee \dots \vee Perm_{n}^{act} (t))
\end{align*}\
where \emph{t} is a token in place \emph{act\_log} containing log information
about  the firing conditions of the incoming transitions. Formulas
$Perm_{1}^{act} (t) \dots Perm_{n}^{act} (t)$ are predicate logic
formulas, one for each permission for activity \emph{act}. Each of those
formulas checks the collected log tokens in \emph{act\_log} for a possible
violations of an access control policy. Note that formulas $Perm_{1}^{act} (t)
 \dots Perm_{n}^{act} (t)$ are disjunct. This is because several permissions amy
 exist for the same activity. Finally the $\bold{AG}$ temporal operator makes
 sure the formula holds for all reachable states of the APN.


%%%%% revised here

After we well constructed the APN model, we are able to draw a subset, focus on
the logs, from the potential total state space of the model. We name it as
``access state space''. Afterwards we can transform access control rules, no
matter permissions or prohibitions, into safety properties of the model on the
access state space. Formally we have
\begin{align*}
Permissions : AG_{logs}(PERM^{\vee}) \\
Prohibitions : AG_{logs}(PROH^{\wedge})
\end{align*}
where the subscript \emph{logs} represents the access state space, and
$PERM^{\vee}/PROH^{\wedge}$ means boolean conjunction of permission/prohibition
rules respectively:
\begin{align*}
PERM^{\vee} = perm_1 \vee perm_2 \vee \ldots \vee perm_m \\
PROH^{\wedge} = proh_1 \wedge proh_2 \wedge \ldots \wedge proh_n
\end{align*}

The safety property transformed from permissions asserts that any state (log) in
the access state space always satisfies at least one of the permission rules. In
other words, all recorded system accesses are explicitly permitted. Similarly
the safety property transformed from prohibitions asserts that any state (log)
in the access state space always satisfies all the prohibition rules (aware that
a prohibition rule is a negative proposition), which means any unsecured system
access would never happen.

\begin{figure}
\centering
\includegraphics[scale=0.5]{./figures/logsSP.jpg}
\caption{Partition of access state space}
\label{fig:./figures/logsSP.jpg}
\end{figure}

Figure \ref{fig:./figures/logsSP.jpg} illustrates the partition of the access
state space in general. The whole area (part I, II, III and IV) represents all
potential logs in the access state space, when there is no security guards
(access control conditions) on transitions. These logs can be divided in two
groups, if the integrity of the access control policies is insured, which are in
consistence with permissions/prohibitions respectively, see the partition by the
horizontal dashed line in Figure \ref{fig:./figures/logsSP.jpg}. If we add the
security guards, to implement the access control policies on the model, some
accesses will be denied so that the corresponding logs will not appear in the
access state space any more, see the right area of the vertical dashed line in
Figure \ref{fig:./figures/logsSP.jpg}.

The safety property, no matter transformed from permissions or prohibitions,
awares globally the logs in the access state space, see the left-slashed shadow
in Figure \ref{fig:./figures/logsSP.jpg}. Therefore when we do model checking of
any safety property, the model checker will report counter-examples of the logs
in part III in Figure \ref{fig:./figures/logsSP.jpg}, say security flaws.


\begin{figure}
\centering
\includegraphics[scale=0.4]{./figures/coEvolution.pdf}
\caption{Safe co-evolution framework}
\label{fig:./figures/coEvolution.pdf}
\end{figure}



Besides these safety properties, we also should define reachability property on
permission rules to insure the system functionality integrity is complete.
Simply say: all permitted system accesses can be eventually conducted. Formally
we have
\begin{align*}
Permissions : EF_{logs}(perm_1) \wedge EF_{logs}(perm_2) \wedge \ldots \wedge
EF_{logs}(perm_m)
\end{align*}




The final ideal access state space is illustrated in Figure
\ref{fig:./figures/finalSP.jpg}.

\begin{figure}
\centering
\includegraphics[scale=0.5]{./figures/finalSP.jpg}
\caption{Transverse momentum distributions}
\label{fig:./figures/finalSP.jpg}
\end{figure}
